the_w:World, l:IdLnk, t:. m(l;t)  (Msg List) 

latex

Definitions	x:A. B(x), t  T, Msg, m(l;t), w.M, onlnk(l;mss), m(i;t), t.1, t.2, S  T, World
Lemmas	filter wf, Msg wf, eq lnk wf, mlnk wf, lsrc wf, Id wf, nat wf, IdLnk wf, world wf